/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package chameleon.model.NuGatStructure.strategy;

import chameleon.model.NuGatStructure.game.GameParams;
import chameleon.model.NuGatStructure.game.GamePlayer;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.opt.OptGame;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.bdd.DdManager;
import chameleon.model.NuGatStructure.enc.BddEnc;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.fsm.BddFsm;
import chameleon.model.NuGatStructure.fsm.GameBddFsm;
import chameleon.model.NuGatStructure.prop.Prop;
import chameleon.model.NuGatStructure.symbTable.SymbLayer;
import chameleon.model.NuGatStructure.utils.Expression;
import chameleon.model.game.Game;
import chameleon.view.OutputManager;
import com.sun.jna.Pointer;

/**
 *
 * @author simon
 */
public class StructCheckLTLGameSF07 extends GameStrategy {
   
    
    //******************* CONSTRUCTOR ***************************************//
    
    public StructCheckLTLGameSF07(Pointer struct, NuGatInterface nugat){
        super(struct,nugat);
        prop_ = new PropGame(nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_get_prop(this.ptr()), nugat_);
    }
    
    public StructCheckLTLGameSF07(PropGame prop,
                                  GameParams params,
                                  int kmin,
                                  int kmax,
                                  int Game_Who_w,
                                  NuGatInterface nugat){
        super(nugat.Game_SF07_StructCheckLTLGameSF07_create(prop.ptr(),
                params.ptr(), kmin, kmax, Game_Who_w),nugat);
        prop_=prop;
    }
    
    //******************** DESTRUCTOR *************************************//
    
    @Override
    public void destroy(){
        nugat_.Game_SF07_StructCheckLTLGameSF07_destroy(this.ptr());
    }
    
    //******************* GETTER ******************************************//
    
    private Pointer getStrategy(){
        return nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_get_strategy(this.ptr());
    }
    
    @Override
    public final GamePlayer getPlayer(){
        return new GamePlayer (nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_get_player(this.ptr()),nugat_);
    }
   
    public final int getStatus(){
        PropGame prop = getProp();
        return prop.getStatus();
    }
    
    @Override
    public final BddEnc getBddEnc(){
        checkStrategyExistence();
        if (enc_ == null)
            enc_ = new BddEnc(nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_get_BddEnc(this.ptr()),nugat_);
        return enc_; 
    }
    
    /**
     *  Synopsis    [ Getter for init_goal ]

        Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    @Override
    public final Bdd getInitGoal(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_init_goal(getStrategy()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for init_opponent_deadlock ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    @Override
    public final Bdd getInitOpponentDeadlock(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_init_opponent_deadlock(getStrategy()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for init_moves ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    @Override
    public final Bdd getInitMoves(){
        checkStrategyExistence();
        return new Bdd (nugat_.GameStrategy_get_init_moves(getStrategy()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for goal ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    @Override
    public final Bdd getGoal(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_goal(getStrategy()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for opponent_deadlock ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    @Override
    public final Bdd getOpponentDeadlock(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_opponent_deadlock(getStrategy()),nugat_);
    }
    
    /**
     * Synopsis    [ Getter for moves ]

       Description [ Result is referenced, i.e., caller obtains ownership. ]
     * @return 
     */
    
    @Override
    public final Bdd getMoves(){
        checkStrategyExistence();
        return new Bdd(nugat_.GameStrategy_get_moves(getStrategy()),nugat_);
    }
   
    public Node getCurrPlayer2MonitorSexpCopy(){
        return new Node (nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_get_curr_player2_monitor_sexp_copy(this.ptr()),nugat_);
    }
    
    public Node getLtlSpec(){
        return new Node(prop_.getExprCore().ptr(),nugat_);
    }
    
    @Override
    protected Bdd getInitBdd(){
        BddEnc enc = getBddEnc();
        DdManager ddManager = enc.getDdManager();
        Bdd init =  ddManager.bddDup(getInitGoal());
        
        init = ddManager.bddOrAccumulate(init, getInitOpponentDeadlock());
        init = ddManager.bddOrAccumulate(init, getInitMoves());
        
        Node iter = getCurrPlayer2MonitorSexpCopy().cdr();
        
        while(iter.notNull()){
            if (iter.car().getType()==nugat_.INIT){
                Bdd newInit = enc.exprToBdd(new Expression(iter.car().car().ptr(),nugat_), 
                        new Node (Pointer.NULL,nugat_));
                init = ddManager.bddOrAccumulate(init, newInit);
            }
            iter = iter.cdr();
        }
        
        return init;
    }
    
    @Override
    protected Bdd getTransBdd(){
        BddEnc enc = getBddEnc();
        DdManager ddManager = enc.getDdManager();
        Bdd trans = ddManager.bddDup(getGoal());
        
        trans = ddManager.bddOrAccumulate(trans, getOpponentDeadlock());
        trans = ddManager.bddOrAccumulate(trans, getMoves());
        
        Node iter = getCurrPlayer2MonitorSexpCopy().cdr();
        
        while(iter.notNull()){
            if (iter.car().getType()==nugat_.TRANS){
                Bdd newTrans = enc.exprToBdd(new Expression(iter.car().car().ptr(),nugat_), 
                        new Node (Pointer.NULL,nugat_));
                trans = ddManager.bddOrAccumulate(trans, newTrans);
            }
            iter = iter.cdr();
        }
        
        return trans;
    }
    
    public SymbLayer getLayerOfPlayer1(){
        return new SymbLayer(nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_get_layer_of_player_1(this.ptr()), nugat_);
    }
    
    public SymbLayer getLayerOfPlayer2(){
        return new SymbLayer(nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_get_layer_of_player_2(this.ptr()), nugat_);
    }
   
    //********************* SETTER ******************************************//
    
    @Override
    public final void setInitGoal(Bdd initGoal){
        nugat_.GameStrategy_set_init_goal(getStrategy(), initGoal.ptr());
    }
    
    @Override
    public final void setInitOpponentDeadlock(Bdd initOpponentDeadlock){
        nugat_.GameStrategy_set_init_opponent_deadlock(getStrategy(), initOpponentDeadlock.ptr());
    }
    
    @Override
    public final void setInitMoves(Bdd initMoves){
        nugat_.GameStrategy_set_init_moves(getStrategy(), initMoves.ptr());
    }
    
    @Override
    public final void setGoal(Bdd goal){
        nugat_.GameStrategy_set_goal(getStrategy(), goal.ptr());
    }
    
    @Override
    public final void setOpponentDeadlock(Bdd opponentDeadlock){
        nugat_.GameStrategy_set_opponent_deadlock(getStrategy(), opponentDeadlock.ptr());
    }
    
    @Override
    public final void setMoves(Bdd moves){
        nugat_.GameStrategy_set_moves(getStrategy(), moves.ptr());
    }
    
    public final void setParams(GameParams params){
        nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_set_params(this.ptr(), params.ptr());
    }
    
    //******************** PRINT METHOD ***********************************//
    
    private void printStrategyMonitorSexp(String file){
        nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_print_strategy_monitor_sexp(this.ptr(),1,0,1,file);
    }
    
    private void printStrategyMonitorBdd(String file){
        nugat_.Chameleon_Game_SF07_StructCheckLTLGameSF07_print_strategy_monitor_bdd(this.ptr(),1,0,1,file);
    }
    
    public final void printStrategy (String file, OptGame opt){
        
        if (opt.getGameSf07StrategyPrintingMode() ==
            nugat_.GAME_SF07_STRATEGY_PRINTING_MODE_SEXP) {
            printStrategyMonitorSexp(file);
        }
        else {
            printStrategyMonitorBdd(file);
        }
        
    }

    @Override
    public final void printStrategy(String file) {
        printStrategyMonitorSexp(file);
    }
    
    @Override
    public final void printStatus(){
        super.printStatus();
        OutputManager output = new OutputManager();
        
        if (StrategyExists()){
              /* strategy reached */if (prop_.getType() == nugat_.PropGame_LtlGame){
                  if (getStatus() == nugat_.Prop_True)
                      output.displayString(" : the strategy has been found\n");
                  else if (getStatus() == nugat_.Prop_False)
                      output.displayString(" : no strategy exists\n");
                  else if (getStatus() == nugat_.Prop_Unchecked)
                      output.displayString(" : existence of a strategy is unknown\n");
              }
          }
          else{
              output.displayString(" : no strategy exists\n");
          }
    }

    @Override
    public void strategyIsWinning(Game game){
        GamePlayer player = getPlayer();
        String strPlayer = player.toString();
        
        
        Node spec = getLtlSpec();
        
        BddFsm playerBddFsm;
        BddFsm opponentBddFsm;
        BddFsm stratBddFsm;
        
        if (strPlayer.equals(nugat_.PLAYER_NAME_1)){
            playerBddFsm = game.getBddFsmP1().clone();
            opponentBddFsm = game.getBddFsmP2().clone();
        }
        else{
            playerBddFsm = game.getBddFsmP2().clone();
            opponentBddFsm = game.getBddFsmP1().clone();
        }
        
        
        //create the strategy bdd fsm
        stratBddFsm = getBddFsm(playerBddFsm, game.getOptsHandlerInstance(),
                game.getGlobalFsmBuilder());
        
        
        
        
        //third Game * strategy
        opponentBddFsm.applySynchronousProduct(stratBddFsm);
        
        opponentBddFsm.checkLtlSpec(new Prop(spec, nugat_.Prop_Ltl, nugat_), 
          game.getPropDatabase());
    }

}
